Example 4 in [Zantema - RTA'97]

Summary: Ex4_Zan97

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (LPO @ AProVE)
  2. Ferreira and Ribeiro's transformation (Corollary)
  3. Giesl and Middeldorp's transformation (Corollary)
  4. CSRPO

CS-TRS Ex4_Zan97 (file Ex4_Zan97.csr)

Functions:  f cons g 0 s sel

Constructors:  cons 0 s

Variables:  X Y Z

Arities: 

ar(f) = 1
ar(cons) = 2
ar(g) = 1
ar(0) = 0
ar(s) = 1
ar(sel) = 2

Replacement map: 

µ(f)={1}
µ(cons)={1}
µ(g)={1}
µ(0)={}
µ(s)={1}
µ(sel)={1,2}

Rules: (file Ex4_Zan97)

f(X) -> cons(X,f(g(X)))
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
sel(0,cons(X,Y)) -> X
sel(s(X),cons(Y,Z)) -> sel(X,Z)

The CS-TRS in OBJ format (file Ex4_Zan97.obj):

obj Ex4_Zan97 is
  sort S .
  op f : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op g : S -> S .
  op 0 : -> S .
  op s : S -> S .
  op sel : S S -> S .
  vars X Y Z : S .
  eq f(X) = cons(X,f(g(X))) .
  eq g(0) = s(0) .
  eq g(s(X)) = s(s(g(X))) .
  eq sel(0,cons(X,Y)) = X .
  eq sel(s(X),cons(Y,Z)) = sel(X,Z) .
endo

Negative results

1. The µ-termination of Ex4_Zan97 cannot be proved by using Lucas' transformation. The TRS Ex4_Zan97_L:

       from(X) -> cons(X)
       g(0) -> s(0)
       g(s(X)) -> s(s(g(X)))
       sel(0,cons(X)) -> X
       sel(s(X),cons(Y)) -> sel(X,Z)
       

   contains extra variables.

Positive results

1. Ex4_Zan97 is proved µ-terminating in [Zan97, Example 4] by using Zantema's transformation. The TRS Ex4_Zan97_Z:

       f(X) -> cons(X,n__f(g(X)))
       g(0) -> s(0)
       g(s(X)) -> s(s(g(X)))
       sel(0,cons(X,Y)) -> X
       sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
       f(X) -> n__f(X)
       activate(n__f(X)) -> f(X)
       activate(X) -> X
       

   is terminating (use LPO with AProVE).
2. By [GM04, Theorem 11], the µ-termination of Ex4_Zan97 can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
3. By [GM04, Theorem 22], the µ-termination of Ex4_Zan97 can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
4. The µ-termination of Ex4_Zan97 can be proved using CSRPO .Proofs : MuTerm and Albert Rubio :
   • marking map:

         m(cons,2)= f
     

   • precedence:

        f > f',cons, g 
        g > s 
        sel > f
     

   • status:

        st(sel) = lex